Nuprl Lemma : es-locl-irreflex-test
11,40
postcript
pdf
es
:ES,
e2
,
e
:E. (
e
<loc
e2
)
(
(
e
=
e2
))
latex
Definitions
,
t
T
,
A
,
P
Q
,
x
:
A
.
B
(
x
)
,
False
Lemmas
event
system
wf
,
es-locl
wf
,
es-E
wf
,
es-locl
irreflexivity
,
es-le
weakening
eq
,
es-locl
transitivity2
origin
es:ES, e2, e:E. (e <loc e2) 
(
(e = e2)) es:ES, e2, e:E. (e <loc e2) ((e = e2)) 
TA Qx:A. B(x)